COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\section{General tree recursion.}
C00013 00003	\section{Non-structural recursions.}
C00018 00004	\section{Solving a \lisp\ programming problem.}
C00030 00005	\noindent{\it Unification}
C00045 ENDMK
C⊗;
\section{General tree recursion.}
\sectlab{treerec}

	A tree structure is either a leaf or a node together with
a collection of immediate successors which are also trees.  Many data structures
can be viewed as trees.  For example, S-expressions are trees with leaves as atoms,
and each non-leaf tree has two successors given by the /car\// and the /cdr/.  
More generally, the structures described in section \sectref{strucrec}
can be thought of as tree-like structures with the basic elements as leaves,
and each non-leaf tree having immediate successors given by the selector
functions for the particular type of node.  These structures all have two things
in common.  Namely, (i) each kind of node has a fixed number of successors and
(ii) these successors are already present as parts of the original tree.

	Another kind of tree is given by an initial position
together with a /successors\// function from which we may obtain the immediate
successors of any position (of relevance).  A node may have any
number of successors, and parts of the trees are built as needed.
Functions on such trees typically involve two processes, one for recognizing
and dealing with leaves and one for processing a collection of succesors.
(Of course the two processes interact recursively.)  

	Consider the problem for searching a tree for a position having some
particular property.   We can write a program that describes a depth
first  search independent of the property or kind of tree.
It can be used to search specific trees  by defining the
three auxiliary functions /successors/, /ter/, and /lose\// for the particular
problem.  We have
\beginlisp
(DEFUN SEARCH (P) (COND ((LOSE P) 'LOSE) ((TER P) P) (T (SEARCHLIS (SUCCESSORS P)))))
(bb tex '(search))
\endlisp
\beginfundef
\funlab{search}
\hskip0\unit /search\// /p\// ← \cr
\hskip4\unit     \qif  /lose\// /p\// \qthen  |LOSE| \qelsif  /ter\// 
/p\// \qthen  /p\// \qelse  /searchlis\// /successors\// /p\//\cr
\endfundef
where
\beginlisp
(DEFUN SEARCHLIS (U) 
  (COND ((NULL U) 'LOSE) 
	(T (LET ((X (SEARCH (CAR U))))
	      (COND ((EQ X 'LOSE)(SEARCHLIS (CDR U))) (T X))))))
(bb tex '(searchlis))
\endlisp
\beginfundef
\funlab{searchlis}
\xx{0} searchlis u ← \cr
\xx{4}     \qif  \qn u \qthen  |LOSE|\cr
\xx{4}     \qelse  \qlet  x ← search \qa u \qin  \qif  x \qeq |LOSE| \qthen 
 searchlis \qd u \qelse  x\cr
\endfundef

In the applications, we start with a position /p0/, and we
are looking for a win in the successor tree of /p0/.  Certain
positions lose and there is no point looking at their successors.
This is decided by the predicate /lose/.  A position is a win if
it doesn't lose and it satisfies the predicate /ter/.  The
successors of a position are given by the function /successors/,
and the value of /search\ p\// is the winning position.  No
non-losing position should have the name |LOSE| or the function won't
work properly.

	One application is finding a path from an initial node to
a final node in a graph represented by a list structure as described
in chapter I\null.  A position is a path starting from the initial node
and continuing to some intermediate node and is represented by a
list of its nodes in reverse order.  The three functions for this
application are
\beginlisp
(DEFUN LOSE (P) (MEMBER (CAR P) (CDR P)))
(DEFUN TER (P) (EQ (CAR P) 'FINAL))
(DEFUN SUCCESSORS 
  (P) (MAPCAR (FUNCTION (LAMBDA (X) (CONS X P)))
                      (CDR (ASSOC (CAR P) GRAPH)))))
(bb tex '(lose ter successors))
\endlisp
\beginfundef \funlab{lose}\funlab{ter}\funlab{successors}
\xx{0} lose p ← \qa p ε \qd p\cr
\noalign{\medskip}
\xx{0} ter p ← \qa p \qeq |FINAL|\cr
\noalign{\medskip}
\xx{0} successors p ← mapcar[[λx: x \qcons  p], \qd assoc[\qa p, graph]]\cr
\endfundef

The node we are proposing to visit next loses if it is already in
the path, as that means we have been here before.  The successors to a position
are all of those positions immediately reachable from the current node.
In our list notation for a graph the immediately reachable nodes are those
on the list associated with the current node in /graph/.  A position is
terminal if the current node is the desired goal |FINAL|.  

	/search\// is used when we want to search a tree of possibilities
for a solution to a problem.
Naturally we can do other things with tree search recursion than just
search.  For example we may want to find all solutions
to a problem.  This can be done with a function /allsol\// that uses
the same /lose/, /ter/, and /successors\// functions as does /search/. 
The simplest way to write /allsol\// is
\beginlisp
(DEFUN ALLSOL1 (P) (COND ((LOSE P) NIL)
		((TER P) (LIST P))
		(T (MAPAPP (FUNCTION ALLSOL1) (SUCCESSORS P)))))
(bb tex '(allsol1))
\endlisp
\beginfundef 
\funlab{allsol}
\hskip0\unit allsol1 p ← \cr
\hskip4\unit     \qif  lose p \qthen  \qNIL \cr
\hskip4\unit     \qelsif  ter p \qthen  <p>\cr
\hskip4\unit     \qelse  mapapp[allsol1, successors 
p]\cr
\endfundef 
where
\beginlisp
(DEFUN MAPAPP (FN U) (COND ((NULL U) NIL) (T (APPEND (FN (CAR U)) 
	(MAPAPP FN (CDR U))))))
(bb tex '(mapapp))
\endlisp
\beginfundef
\funlab{mapapp}
\hskip0\unit /mapapp\//[/fn\//, /u\//] ← \qif  \qn /u\// \qthen 
 \qNIL  \qelse  /fn\// \qa /u\// * /mapapp\//[/fn\//, \qd /u\//]\cr
\endfundef

This form of the function is somewhat inefficient because of all the
/append\//ing.  A more efficient form uses an auxiliary function as follows: 
\beginlisp
(DEFUN ALLSOL (P) (ALLSOLA P NIL))
;
(DEFUN ALLSOLA (P FOUND) (COND
	((LOSE P) FOUND)
	((TER P) (CONS P FOUND))
	(T (ALLSOLB (SUCCESSORS P) FOUND))))
;
(DEFUN ALLSOLB (U FOUND) (COND
	((NULL U) FOUND)
	(T (ALLSOLB (CDR U) (ALLSOLA (CAR U) FOUND)))))
(bb tex '(allsol allsola allsolb))
\endlisp
\beginfundef \funlab{allsola}
\hskip0\unit /allsol\// /p\// ← /allsola\//[/p\//, \qNIL ]\cr
\noalign{\medskip}
\hskip0\unit /allsola\//[/p\//, /found\//] ← \cr
\hskip4\unit     \qif  /lose\// /p\// \qthen  /found\//\cr
\hskip4\unit     \qelsif  /ter\// /p\// \qthen  /p\// \qcons  /found\//\cr
\hskip4\unit     \qelse  /allsolb\//[/successors\// /p\//, /found\//]\cr
\noalign{\medskip}
\hskip0\unit /allsolb\//[/u\//, /found\//] ← \qif  \qn /u\// \qthen 
 /found\// \qelse  /allsolb\//[\qd /u\//, /allsola\//[\qa /u\//, /found\//]]\cr
\endfundef 

The recursive program structure that arises here is common when a list
is to be formed by recurring through a list structure.

	We will give further applications of and variations on this form
of tree search recursion in chapter \chapref{search}.
\section{Non-structural recursions.}
\sectlab{nonstruc}
	Not all recursions are structural.  It is quite possible to
define recursive functions which are not in any of the special forms
already mentioned.  The drawback is that
there is no reason to assume that the computation will terminate.

	For example,
\beginlisp
(DEFUN F (N) (COND ((EQUAL N 1) 1) ((EVEN N) (F (// N 2))) 
    (T (F (PLUS (TIMES 3 N) 1)))))
(bb tex '(f))
\endlisp
\beginfundef 
% Definition changed to give n/2 and 3n+1 in nicer notation
\hskip0\unit /f/ /n/ ← \cr
\hskip4\unit     \qif  /n/ \qequal 1 \qthen  1\cr
\hskip4\unit     \qelsif  /even/ /n/ \qthen  /f/ [/n/\div 2]\cr
\hskip4\unit     \qelse  /f/ [3n + 1]\cr
\endfundef 
terminates for all positive integer values of /n\// that have been tested,
but no-one has been able to determine whether it always terminates.  If
you want to experiment, try small values of /n/ to get an idea of how the
function seems to behave, and then try $/n/=27$.

	The function
\beginlisp
(DEFUN SACK (X Y) 
    (COND ((ATOM X) (CONS X Y))
	((ATOM Y) (SACK (CAR X) (CDR X)))
	(T (SACK (CDR X) (SACK X (CDR Y))))))
(bb tex '(sack))
\endlisp
\beginfundef 
\hskip0\unit /sack/[/x/, /y\//] ← \cr
\hskip4\unit     \qif  \qat /x/ \qthen  /x/ \qcons  /y/\cr
\hskip4\unit     \qelsif  \qat /y/ \qthen  /sack/[\qa /x/, \qd /x\//]\cr
\hskip4\unit     \qelse  /sack/[\qd /x/, /sack/[/x/, \qd /y\//]]\cr
\endfundef 
is an S-expression analog of the function /ack\// defined in 
section \sectref{numrec}
on numerical recursion.  Unlike /flat\// the occurrence of double recursion
$(/sack/[\ldots,/sack/[\ldots]])$ is crucial.  Like /ack\// this function cannot
be defined by any collection of simple recursive schemata.
It is a kind of structural recursion.

	Takeuchi defined the function
\beginlisp
(DEFUN TAK (X Y Z)
    (COND ((GREATERP X Y) (TAK (TAK (DIFFERENCE X 1) Y Z)
			       (TAK (DIFFERENCE Y 1) Z X)
			       (TAK (DIFFERENCE Z 1) X Y)))
	  (T Z)))
(bb tex '(tak))
\endlisp
\beginfundef 
\hskip0\unit /tak/[/x/, /y/, /z\//] ← \cr
\hskip4\unit     \qif  /x/ \qgt  /y/ \qthen  \cr
\hskip8\unit         /tak/[/tak/[/x/ \minus 1, /y/, /z\//], \cr
\hskip14\unit               /tak/[/y/ \minus 1, /z/, /x\//], \cr
\hskip14\unit               /tak/[/z/ \minus 1, /x/, /y\//]]\cr
\hskip4\unit     \qelse  /z/\cr
\endfundef 
to test \lisp\ systems on a program that would run a long time but not
use much storage or stack.  It has been shown to terminate for all
integer arguments.  Most likely it also always terminates for real
arguments, but this seems harder to show.

	The interpreter /eval\// is itself a non-structural recursion,
and whether it terminates depends on the expressions it is given
to evaluate.
\section{Solving a \lisp\ programming problem.}
\sectlab{soln}

	In this section we present two programming problems
that are somewhat more complex than those of the earlier sections.
We work out the solutions in detail.  The purpose is to help the reader
think recursively and to show how a typical problem
might be approached.
The first problem is really a simpler version of the second problem.
Its solution helps in understanding the
various aspects of the control structure and information
flow needed in the second problem.    

\noindent{\it Pattern Matching}

        Pattern matching is fundamental to several parts of
computer science.  Examples are
simplifying arithmetic expressions, natural language parsing,
theorem proving systems and compilers.
We will consider a simplified version of the pattern matchers suggested 
by these examples.

	A {\it pattern\/} is an S-expression containing 
(zero or more) {\it variables}.  
For us the
variables are simply atoms which have been designated as such by
some predicate which we call $isvar$.
An {\it instance}
of the pattern is obtained by substituting S-expressions for the variables.

	Since the pattern may have several variables, we use a function
$sublis$ that substitutes simultaneously for all the variables in an
association list.  It is defined by
%
\beginlisp
(defun sublis (p al)
  (if (atom p)
      (if (isvar p) 
          (let ((w (assoc p al)))  (if (null w) p (cdr w)))
          p)
      (cons (sublis (car p) al) (sublis (cdr p) al))))
(bb tex '(sublis))
\endlisp
%
\beginfundef
\xx{0} sublis[p, al] ← \cr
\xx{4}     \qif  \qat p \qthen  \cr
\xx{8}         [\qif  isvar p \qthen  \qlet  w ← assoc[p, al] \qin  \qif 
 \qn w \qthen  p \qelse  \qd w\cr
\xx{9}          \qelse  p]\cr
\xx{4}     \qelse  sublis[\qa p, al] \qcons  sublis[\qd p, al].\cr
\endfundef

	Matching may therefore be described as an inverse of $sublis$.  The
function $match$ should return an association list if the match is successful.
An unsuccessful attempt
is signified by returning the atom |NO|.  One cannot simply return |NIL|
to indicate failure to match,
because |NIL| is a possible successful answer.  The recursion that defines
$match$ requires that $match$ has an association list $al$ as a third argument.
$al$ contains the variable-value pairs to which $match$ is already committed.
Therefore, $match[p,e,al]$ must be defined so that if the match is successful
we have
%
$$sublis[p,match[p,e,al]] = e,$$
%
whereas if the match fails $match[p,e,al] = |NO|$.

\noindent{\it Examples of the use of /match/}

\nobreak
To make the above description of /match\// clearer, consider the
problem of checking
whether a function definition is of a 
particular form.  (This suggests the possibility of using pattern matching 
in compiling to recognize particular forms which can then
be given special treatment.)

We want to recognize (internal) function definitions with a form which
might be called {\it right-first tree processing}.  Functions in this
form process the cdr of their argument first, and then use the result
to process the car of the argument.
So we need a pattern with variables for the name of the function,
the two arguments, and the then-part of the expression.  We will call
these variables |name|, |arg|, |parameter| and |then|.  With those
variables our pattern is
\medskip
\begindefun
(DEFUN name (arg parameter) 
   (IF (ATOM arg) then (name (CAR arg) (name (CDR arg) parameter)))).
\enddefun
The function $flat$, which was defined as function \funref{flatten}, has
this form:
\begindefun
(DEFUN FLAT (X U)
   (IF (ATOM X) (CONS X U)
                (FLAT (CAR X) (FLAT (CDR X) U))))
\enddefun
$match$ing the pattern and the constant gives
$$
\iffalse % comment this out for the moment, should be thrown away.
\eqalign{
&match[\cr
&|     (DEFUN NAME (ARG PARAMETER) |\cr
&|        (IF (ATOM ARG) THEN (NAME (CAR ARG) (NAME (CDR ARG) PARAMETER))))|,\cr
\cr
&|     (DEFUN FLAT (X U)|\cr
&|        (IF (ATOM X) (CONS X U)|\cr
&|                     (FLAT (CAR X) (FLAT (CDR X) U))))|\cr
\cr
&|    NIL|]\cr
\cr
&=
\fi
|((then . (CONS X Y)) (parameter . Y) (arg . X) (name . FLAT))| .
%\cr}
$$


Now we describe the algorithm to be used.  If $al$
is |NO| then no binding is possible and $match$ should return |NO|
immediately.
If $x$ is an atom, but not a variable,
$match[x,y,al]$ succeeds if $x\qeq y$ and fails otherwise.  If $x$ is a
variable we must check its binding in $al$.  If it has none, then $match$
returns $al$ extended by $[x\qcons y]$.  If there is already a binding
for $x$, and it is equal to $y$, there is no need to add anything to $al$, 
but if the existing binding is not equal to $y$, there can be no match, and
$match$ must return |NO|.  

If $x$ is a pair, and $y$ is an atom, the match fails.  If $x$ and $y$ are both
pairs, we call $match$ recursively.  That is we evaluate $match[\qa x,
\qa y,al]$.  This returns a binding list, which we then pass to
a second call of $match$, this time to try to match 
$\qd x$ and $\qd y$.

\noindent{\it The /match/ program}


The following is our solution to this programing problem. 
Notice that
it is not really important how $isvar$ is defined, beyond knowing
that $/isvar/[\qNIL]=\qNIL$ and
that $/isvar/[x]= \qT$ implies $/at/[x] = \qT$.
%
\beginlisp
(defun match (p e al) 
  (if (eq al 'NO)
      'no
      (if (atom p)
          (if (isvar p)
              (let ((w (assoc p al))) (if (null w)
                                         (cons (cons p e) al)
                                         (if (equal (cdr w) e)
                                             al
                                             'no)))
              (if (eq p e) al 'no))
          (if (atom e)
              'no
              (match (cdr p)
                     (cdr e)
                     (match (car p) (car e) al))))))
(bb tex '(match))
\endlisp
\beginfundef
\xx{0} match[p, e, al] ← \cr
\xx{4}     \qif  al \qeq |NO| \qthen  |NO|\cr
\xx{4}     \qelsif  \qat p \qthen  \cr
\xx{8}         [\qif  isvar p \qthen  \cr
\xx{12}             \qlet  w ← assoc[p, al] \cr
\xx{16}                 \qin  \qif  \qn w \qthen  [p \qcons  e] \qcons al \cr
\xx{18}                    \qelsif  \qd w \qequal e \qthen  al \qelse  |NO|\cr
\xx{9}          \qelsif  p \qeq e \qthen  al\cr
\xx{9}          \qelse  |NO|]\cr
\xx{4}     \qelsif  \qat e \qthen  |NO|\cr
\xx{4}     \qelse  match[\qd p, \qd e, match[\qa p, \qa e, al]]\cr
\endfundef


\noindent{\it Unification}

Our next problem can be considered an extension of the
match problem.  The problem arises naturally in automatic deduction
systems based on Robinsons {\it resolution} principle.
Unification is also the basis of the Prolog programming language.
In these systems propositions may be represented as  
patterns in which the pattern variables represent universally quantified
variables.  The unification problem arises when a program must determine whether
two patterns each represent an instance of the ``same'' proposition.  

Another way to state this problem is as follows.
Suppose that $x↓1$ and $x↓2$ are patterns, we say that
an association list $al$ unifies $x↓1$ and $x↓2$ if the result of carrying out the
substitutions given by $al$ in $x↓1$ is equal to the result of carrying out the same
substitutions in $x↓2$.  We always assume that if a variable is unbound no
substitution is made for it.

For example, let |x| and |y| be pattern variables, and |<|, |F| and |G| be
constants.
The patterns |(< x (F x))| and
|(< (G y) (F (G y))| are unified by binding |x| to |(G y)|.  In general
we have to give bindings for variables from
both patterns, as in |(< (F x) x)| and |(< y A)|.  Here we must
bind |x| to |A| and |y| to |(F A)|.

When we defined $match$ we added a new binding by $cons$ing it onto
the existing alist.  The situation with $uni$ is more complex,
as may be illustrated by the last example.  Suppose we build up
an alist by moving from left to right 
through the lists of that example.  We first
find that |y| must be bound to |(F x)|.  Next, we find that |x| must
be bound to |A|.  Not only must we add this binding
to the alist, we must also update the entry for |y| to |(F A)| instead
of |(F x)|.  In general, when a new entry is added to the alist, all
occurrences of the newly bound variable must be replaced by the variable's
binding.
We will perform this replacement using an
auxiliary function $compose[al, bl]$ which adds the new bindings in
$bl$ to the list $al$, makes any necessary substitutions in $al$ and 
returns the new list as its value.

A second important point concerns the detection of a failure to unify.
For example,
the lists |(< x (F x))| and |(< (G y) y)| cannot be unified.
We could only unify them if |x| were bound to 
|(G y)|, and |y| were bound to |(F x)|.  But the second binding
requires that |x| instead be bound to |(G (F x))|.  At this point
unification fails.  In fact, unification always fails if a variable
must be bound to a value
containing the variable itself.
The test to detect this failure is called the {\it occur check}.
%We shall specify a program /unify/ such that if $/unify/[x↓1,\ x↓2] \not= |NO|$
%then 
%$$/sublis/[x↓1,\ /unify/[x↓1,\ x↓2]] =
%/sublis/[x↓2,\ /unify/[x↓1,\ x↓2]]$$

We now proceed to the definition of a function $unify$ satisfying these
requirements.  We will take the same approach we used with $match$,
namely, we will have $unify$ return the alist of bindings if they are
possible, and the atom |NO| otherwise, and we will introduce a function
$uni$, which is like $unify$ but takes as a third argument an alist
containing the bindings already found.  This gives us
\beginlisp
(defun unify (x y) (uni x y nil))
(bb tex '(unify))
\endlisp
\beginfundef
\xx{0} unify[x, y] ← uni[x, y, \qNIL ]\cr
\endfundef


We begin defining $uni[x,y,al]$, as usual, by considering the base cases.  The 
simplest case is when $al$ is |NO|, for then $uni$ just returns |NO| itself.
The next series of cases is when either $x$ or $y$ is an atom.  

{\it Case 1.} Suppose $x$ and $y$ are both atoms. There are several subcases
depending on whether these atoms are variables or not.  If neither is a
variable, then $x$ and $y$ can only unify if $x \qeq y$, and then $uni[x,y,al]
=al$.  If $x$ is a variable, we can
unify if it is already bound to $y$ (and $uni$ should return $al$), or if
$x$ is unbound.  Then $uni$ should bind $x$ to $y$, if $y$ is unbound, and
to the binding of $y$ if $y$ is bound.

{\it Case 2.} Suppose $x$ is an atom, but $y$ is not.  If $x$ is not
a variable the unification fails, and if $x$ is already bound to $y$ we
are done.  But even if $x$ is bound to something different to $y$, we
may not have failed, because all we need is that $y$ can be {\it unified
with} the value of $x$.  This recursive call to $unify$ is very messy.
and we avoid it by making a change to our strategy.  We insist that in
any call of $uni[x,y,al]$
the variables occurring in $x$ and $y$ do not have any bindings in $al$.

This change in strategy makes some obvious changes to case 1, and means
that in case 2 $x$ can be assumed to be unbound.  So all we have to
do is make the
occur check, (that is, make sure $x$ does not occur anywhere in $y$) and
then (if successful) call $compose[al,<x\qcons y>]$.  We will leave
the task of the occur check to an auxiliary function $occur$.  

{\it Case 3.} This case arises when $y$ is an atom, but $x$ is not.  It
is completely symmetrical with case 2.

Finally, we consider the recursion step.  In the definition of /match\//
we matched $\qa x$ with $\qa y$, and used the resulting alist to try
to match $\qd x$ and $\qd y$.  We can use the same approach for $uni$,
but must take care to remove any occurrences of the newly bound
variables from the two patterns before attempting to call $uni$.  To
that end we will use an auxiliary function $sublis$, where 
$sublis[x,al]$ returns a list where all occurrences of the variables
in $x$  are replaced by their bindings.

The preceding discussion leads to this program:
\beginlisp
(defun uni (x y al)
  (cond ((or (eq al 'no) (eq x y)) al)
        ((isvar x) (if (occur x y) 'no (compose al (list (cons x y)))))
        ((isvar y) (if (occur y x) 'no (compose al (list (cons y x)))))
        ((or (atom x) (atom y)) 'no)
        ( T (let ((bl (uni (car x) (car y) al)))
              (if (eq bl 'no)
                  'no
                  (uni (sublis (cdr x) bl)
                       (sublis (cdr y) bl)
                       bl) ) ) ) ) )
(bb tex '(uni))
\endlisp
\beginfundef
\xx{0} uni[x, y, al] ← \cr
\xx{4}     \qif  al \qeq |NO| \qor  x \qeq y \qthen  al\cr
\xx{4}     \qelsif  isvar x \qthen  \cr
\xx{8}         [\qif  occur[x, y] \qthen  |NO| \qelse  compose[al, <x \qcons 
 y>]]\cr
\xx{4}     \qelsif  isvar y \qthen  \cr
\xx{8}         [\qif  occur[y, x] \qthen  |NO| \qelse  compose[al, <y \qcons 
 x>]]\cr
\xx{4}     \qelsif  \qat x \qor  \qat y \qthen  |NO|\cr
\xx{4}     \qelse  \qlet  bl ← uni[\qa x, \qa y, al] \cr
\xx{8}         \qin  \qif  bl \qeq |NO| \qthen  |NO|\cr
\xx{11}            \qelse  uni[sublis[\qd x, bl], sublis[\qd y, bl], bl]\cr
\endfundef

The algorithm this program implements is called the {\it left-first mesh
substitution}. It does a /left-first/ search for a point of disagreement
between $x$ and $y$. If it fails to find one then of course $x$ and $y$ are
already equal. So, presuming that it discovers a point of disagreement
between $x$ and $y$, it then checks to see if this disagreement is
removable by assigning a value to a pattern variable. If so, it extends the alist
appropriately. Then before backtracking and proceeding with the rest of $x$ and $y$
it makes the forced substitutions. If it cannot rectify the disagreement it
immediately returns |NO|.


The auxiliary function $sublis$ has already been defined.
$occur$ and $compose$ can be defined as follows.
Recall that $occur[x,y]$ checks whether the atom $x$ occurs anywhere in
$y$; $sublis[x, al]$ makes all possible substitutions from the alist $al$
into $x$; and $compose[al, bl]$ adds the new bindings from $bl$ onto the
alist $al$, while substituting new bound values into bindings in $al$.
\beginlisp
(defun occur (x y)
  (if (atom y)
      (eq x y)
      (or (occur x (car y))
          (occur x (cdr y))) ) )
(defun compose (a b) (append (subsub a b) b))
(defun subsub (a b) (if (null a) a (cons (cons (caar a) (sublis (cdar a) b))
                                         (subsub (cdr a) b))))
(bb tex '(occur compose subsub))
\endlisp
\beginfundef
\xx{0} occur[x, y] ← \qif  \qat y \qthen  x \qeq y \qelse  occur[x, \qa 
y] \qor  occur[x, \qd y]\cr
\noalign{\medskip}
\xx{0} compose[a, b] ← subsub[a, b] * b\cr
\noalign{\medskip}
\xx{0} subsub[a, b] ← \qif  \qn a \qthen  a \qelse  [\qaa a \qcons  sublis[\qda 
a, b]] \qcons  subsub[\qd a, b]\cr
\endfundef

%Check whether the corrections to mathmode work

%Add another example to the match section

%Change the flatten example to something more significant